You're reading an old version of this documentation.
For the latest stable release version, please have a look at master.

Dismiss

Formal

General

There is limited support for SystemVerilog Assertions (SVA).

You can add formal statements (assume, assert, etc.) in the Component definition, like in the example below:

class TopLevel extends Component {
  val io = new Bundle {
    val ready = in Bool()
    val valid = out Bool()
  }
  val valid = RegInit(False)

 when(io.ready) {
   valid := False
 }
 io.valid <> valid
 // some logic

 import spinal.core.GenerationFlags._
 import spinal.core.Formal._

 GenerationFlags.formal {
   when(initstate()) {
     assume(clockDomain.isResetActive)
     assume(io.ready === False)
   }.otherwise {
     assert(!(valid.fall && !io.ready))
   }
 }
}

To generate a design which includes the formal statements you can use includeFormal:

object MyToplevelSystemVerilogWithFormal {
 def main(args: Array[String]) {
   val config = SpinalConfig(defaultConfigForClockDomains = ClockDomainConfig(resetKind=SYNC, resetActiveLevel=HIGH))
    config.includeFormal.generateSystemVerilog(new TopLevel())
  }
}

Supported features

Syntax	Returns	Creates in SystemVerilog
assert()		assert()
cover()		cover()
past(that : T, delay : Int) past(that : T)	T	past(that)
rose(that : Bool)	Bool	rose(that)
fell(that : Bool)	Bool	fell(that)
changed(that : Bool)	Bool	changed(that)
stable(that : Bool)	Bool	stable(that)
initstate()	Bool	$initstate()

Limitations

No support for unclocked assertions. Everything that is described in GenerationFlags.formal will be generated in a clocked process.